T:Type. 
subtype_rel(T; )  (x:T, L:(T List), z:T. (z  s-insert(x; L))  ((z = x)  (z  L))) 

latex

Definitions	t  T, prop{i:l}, x:A. B(x), P  Q, P  Q, guard(T), P  Q, (x  l), P  Q, P  Q, False, A, A  B, , A c B, x:A. B(x), s-insert(x; l), sq_type(T), True, i z j, b, b, , i <z j, T, Unit, (i = j)
Lemmas	assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, not wf, eqtt to assert, assert of lt int, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, le wf, bool wf, bnot wf, assert wf, le int wf, member singleton, iff transitivity, iff functionality wrt iff, or functionality wrt iff, cons member, iff wf, nil member, s-insert wf, l member wf